The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

minus(x, 0) → x
minus(s(x), s(y)) → minus(x, y)
double(0) → 0
double(s(x)) → s(s(double(x)))
plus(0, y) → y
plus(s(x), y) → s(plus(x, y))
plus(s(x), y) → plus(x, s(y))
plus(s(x), y) → s(plus(minus(x, y), double(y)))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
plus(0, y) → y [1]
plus(s(x), y) → s(plus(x, y)) [1]
plus(s(x), y) → plus(x, s(y)) [1]
plus(s(x), y) → s(plus(minus(x, y), double(y))) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

minus(x, 0) → x [1]
minus(s(x), s(y)) → minus(x, y) [1]
double(0) → 0 [1]
double(s(x)) → s(s(double(x))) [1]
plus(0, y) → y [1]
plus(s(x), y) → s(plus(x, y)) [1]
plus(s(x), y) → plus(x, s(y)) [1]
plus(s(x), y) → s(plus(minus(x, y), double(y))) [1]

The TRS has the following type information:

minus :: 0:s → 0:s → 0:s 0 :: 0:s s :: 0:s → 0:s double :: 0:s → 0:s plus :: 0:s → 0:s → 0:s

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The TRS is a completely defined constructor system, as every type has a constant constructor and the following rules were added:

minus(v0, v1) → null_minus [0]
double(v0) → null_double [0]
plus(v0, v1) → null_plus [0]

And the following fresh constants:

null_minus, null_double, null_plus

(6) Obligation:

Runtime Complexity Weighted TRS where all functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: minus(x, 0) → x [1] minus(s(x), s(y)) → minus(x, y) [1] double(0) → 0 [1] double(s(x)) → s(s(double(x))) [1] plus(0, y) → y [1] plus(s(x), y) → s(plus(x, y)) [1] plus(s(x), y) → plus(x, s(y)) [1] plus(s(x), y) → s(plus(minus(x, y), double(y))) [1] minus(v0, v1) → null_minus [0] double(v0) → null_double [0] plus(v0, v1) → null_plus [0] The TRS has the following type information: minus :: 0:s:null_minus:null_double:null_plus → 0:s:null_minus:null_double:null_plus → 0:s:null_minus:null_double:null_plus 0 :: 0:s:null_minus:null_double:null_plus s :: 0:s:null_minus:null_double:null_plus → 0:s:null_minus:null_double:null_plus double :: 0:s:null_minus:null_double:null_plus → 0:s:null_minus:null_double:null_plus plus :: 0:s:null_minus:null_double:null_plus → 0:s:null_minus:null_double:null_plus → 0:s:null_minus:null_double:null_plus null_minus :: 0:s:null_minus:null_double:null_plus null_double :: 0:s:null_minus:null_double:null_plus null_plus :: 0:s:null_minus:null_double:null_plus Rewrite Strategy: INNERMOST

(7) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

0 => 0
null_minus => 0
null_double => 0
null_plus => 0

(8) Obligation:

Complexity RNTS consisting of the following rules:

double(z) -{ 1 }→ 0 :|: z = 0
double(z) -{ 0 }→ 0 :|: v0 >= 0, z = v0
double(z) -{ 1 }→ 1 + (1 + double(x)) :|: x >= 0, z = 1 + x
minus(z, z') -{ 1 }→ x :|: x >= 0, z = x, z' = 0
minus(z, z') -{ 1 }→ minus(x, y) :|: z' = 1 + y, x >= 0, y >= 0, z = 1 + x
minus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
plus(z, z') -{ 1 }→ y :|: y >= 0, z = 0, z' = y
plus(z, z') -{ 1 }→ plus(x, 1 + y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
plus(z, z') -{ 0 }→ 0 :|: v0 >= 0, v1 >= 0, z = v0, z' = v1
plus(z, z') -{ 1 }→ 1 + plus(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
plus(z, z') -{ 1 }→ 1 + plus(minus(x, y), double(y)) :|: x >= 0, y >= 0, z = 1 + x, z' = y

Only complete derivations are relevant for the runtime complexity.

(9) CompleteCoflocoProof (EQUIVALENT transformation)

Transformed the RNTS (where only complete derivations are relevant) into cost relations for CoFloCo:

eq(start(V, V1),0,[minus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(start(V, V1),0,[double(V, Out)],[V >= 0]). eq(start(V, V1),0,[plus(V, V1, Out)],[V >= 0,V1 >= 0]). eq(minus(V, V1, Out),1,[],[Out = V2,V2 >= 0,V = V2,V1 = 0]). eq(minus(V, V1, Out),1,[minus(V3, V4, Ret)],[Out = Ret,V1 = 1 + V4,V3 >= 0,V4 >= 0,V = 1 + V3]). eq(double(V, Out),1,[],[Out = 0,V = 0]). eq(double(V, Out),1,[double(V5, Ret11)],[Out = 2 + Ret11,V5 >= 0,V = 1 + V5]). eq(plus(V, V1, Out),1,[],[Out = V6,V6 >= 0,V = 0,V1 = V6]). eq(plus(V, V1, Out),1,[plus(V7, V8, Ret1)],[Out = 1 + Ret1,V7 >= 0,V8 >= 0,V = 1 + V7,V1 = V8]). eq(plus(V, V1, Out),1,[plus(V9, 1 + V10, Ret2)],[Out = Ret2,V9 >= 0,V10 >= 0,V = 1 + V9,V1 = V10]). eq(plus(V, V1, Out),1,[minus(V11, V12, Ret10),double(V12, Ret111),plus(Ret10, Ret111, Ret12)],[Out = 1 + Ret12,V11 >= 0,V12 >= 0,V = 1 + V11,V1 = V12]). eq(minus(V, V1, Out),0,[],[Out = 0,V13 >= 0,V14 >= 0,V = V13,V1 = V14]). eq(double(V, Out),0,[],[Out = 0,V15 >= 0,V = V15]). eq(plus(V, V1, Out),0,[],[Out = 0,V16 >= 0,V17 >= 0,V = V16,V1 = V17]). input_output_vars(minus(V,V1,Out),[V,V1],[Out]). input_output_vars(double(V,Out),[V],[Out]). input_output_vars(plus(V,V1,Out),[V,V1],[Out]).

CoFloCo proof output:
Preprocessing Cost Relations
=====================================

#### Computed strongly connected components
0. recursive : [double/2]
1. recursive : [minus/3]
2. recursive : [plus/3]
3. non_recursive : [start/2]

#### Obtained direct recursion through partial evaluation
0. SCC is partially evaluated into double/2
1. SCC is partially evaluated into minus/3
2. SCC is partially evaluated into plus/3
3. SCC is partially evaluated into start/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations double/2
* CE 8 is refined into CE [16]
* CE 10 is refined into CE [17]
* CE 9 is refined into CE [18]


### Cost equations --> "Loop" of double/2
* CEs [18] --> Loop 11
* CEs [16,17] --> Loop 12

### Ranking functions of CR double(V,Out)
* RF of phase [11]: [V]

#### Partial ranking functions of CR double(V,Out)
* Partial RF of phase [11]:
- RF of loop [11:1]:
V


### Specialization of cost equations minus/3
* CE 7 is refined into CE [19]
* CE 5 is refined into CE [20]
* CE 6 is refined into CE [21]


### Cost equations --> "Loop" of minus/3
* CEs [21] --> Loop 13
* CEs [19] --> Loop 14
* CEs [20] --> Loop 15

### Ranking functions of CR minus(V,V1,Out)
* RF of phase [13]: [V,V1]

#### Partial ranking functions of CR minus(V,V1,Out)
* Partial RF of phase [13]:
- RF of loop [13:1]:
V
V1


### Specialization of cost equations plus/3
* CE 15 is refined into CE [22]
* CE 11 is refined into CE [23]
* CE 12 is refined into CE [24]
* CE 14 is refined into CE [25,26,27,28,29]
* CE 13 is refined into CE [30]


### Cost equations --> "Loop" of plus/3
* CEs [29] --> Loop 16
* CEs [30] --> Loop 17
* CEs [28] --> Loop 18
* CEs [27] --> Loop 19
* CEs [26] --> Loop 20
* CEs [24,25] --> Loop 21
* CEs [22] --> Loop 22
* CEs [23] --> Loop 23

### Ranking functions of CR plus(V,V1,Out)
* RF of phase [16,17,18,21]: [V,2*V-1]

#### Partial ranking functions of CR plus(V,V1,Out)
* Partial RF of phase [16,17,18,21]:
- RF of loop [16:1]:
V+V1-2
V/3-V1/3
- RF of loop [16:1,18:1]:
V/2-1/2
- RF of loop [17:1,21:1]:
V
- RF of loop [18:1]:
V-V1
V1 depends on loops [16:1,17:1]


### Specialization of cost equations start/2
* CE 2 is refined into CE [31,32,33]
* CE 3 is refined into CE [34,35]
* CE 4 is refined into CE [36,37,38,39,40,41]


### Cost equations --> "Loop" of start/2
* CEs [31] --> Loop 24
* CEs [32,33,34,35,36,37,38,39,40,41] --> Loop 25

### Ranking functions of CR start(V,V1)

#### Partial ranking functions of CR start(V,V1)


Computing Bounds
=====================================

#### Cost of chains of double(V,Out):
* Chain [[11],12]: 1*it(11)+1
Such that:it(11) =< Out/2

with precondition: [Out>=2,2*V>=Out]

* Chain [12]: 1
with precondition: [Out=0,V>=0]


#### Cost of chains of minus(V,V1,Out):
* Chain [[13],15]: 1*it(13)+1
Such that:it(13) =< V1

with precondition: [V=Out+V1,V1>=1,V>=V1]

* Chain [[13],14]: 1*it(13)+0
Such that:it(13) =< V1

with precondition: [Out=0,V>=1,V1>=1]

* Chain [15]: 1
with precondition: [V1=0,V=Out,V>=0]

* Chain [14]: 0
with precondition: [Out=0,V>=0,V1>=0]


#### Cost of chains of plus(V,V1,Out):
* Chain [[16,17,18,21],23]: 3*it(16)+4*it(17)+3*it(18)+2*s(8)+1*s(10)+1
Such that:it(18) =< V-V1
aux(15) =< V+V1
it(16) =< V/3-V1/3
aux(22) =< V
aux(23) =< 2*V
aux(24) =< V/2
aux(25) =< V1
aux(26) =< 2*V1
it(16) =< aux(23)
it(16) =< aux(22)
it(17) =< aux(22)
it(18) =< aux(22)
s(8) =< aux(22)
it(18) =< aux(23)
it(17) =< aux(23)
it(16) =< aux(15)
it(18) =< aux(15)
it(16) =< aux(24)
it(18) =< aux(24)
aux(6) =< aux(22)*2
it(18) =< it(17)+aux(22)+aux(25)
s(10) =< it(17)*2+aux(6)+aux(26)
s(10) =< it(18)*aux(15)

with precondition: [V1>=0,Out>=1,Out+V>=V1+2,V+V1>=Out]

* Chain [[16,17,18,21],22]: 3*it(16)+4*it(17)+3*it(18)+2*s(8)+1*s(10)+0
Such that:it(18) =< V-V1
aux(15) =< V+V1
it(16) =< V/3-V1/3
aux(27) =< V
aux(28) =< 2*V
aux(29) =< V/2
aux(30) =< V1
aux(31) =< 2*V1
it(16) =< aux(28)
it(16) =< aux(27)
it(17) =< aux(27)
it(18) =< aux(27)
s(8) =< aux(27)
it(18) =< aux(28)
it(17) =< aux(28)
it(16) =< aux(15)
it(18) =< aux(15)
it(16) =< aux(29)
it(18) =< aux(29)
aux(6) =< aux(27)*2
it(18) =< it(17)+aux(27)+aux(30)
s(10) =< it(17)*2+aux(6)+aux(31)
s(10) =< it(18)*aux(15)

with precondition: [V>=1,V1>=0,Out>=0,V>=Out]

* Chain [[16,17,18,21],20,23]: 3*it(16)+1*it(17)+3*it(18)+3*it(21)+2*s(8)+1*s(10)+1*s(11)+3
Such that:it(18) =< V-V1
it(16) =< V/3-V1/3
aux(32) =< V
aux(33) =< V+V1
aux(34) =< 2*V
aux(35) =< V/2
aux(36) =< V1
aux(37) =< 2*V1
s(11) =< aux(33)
it(16) =< aux(34)
it(16) =< aux(32)
it(17) =< aux(32)
it(18) =< aux(32)
it(21) =< aux(32)
s(8) =< aux(32)
it(18) =< aux(34)
it(21) =< aux(34)
it(16) =< aux(33)
it(18) =< aux(33)
it(21) =< aux(33)
it(17) =< aux(34)
it(16) =< aux(35)
it(18) =< aux(35)
aux(6) =< aux(32)*2
it(18) =< it(17)+aux(32)+aux(36)
s(10) =< it(17)*2+aux(6)+aux(37)
s(10) =< it(18)*aux(33)

with precondition: [V>=2,V1>=0,Out>=1,V>=Out]

* Chain [[16,17,18,21],20,22]: 3*it(16)+1*it(17)+3*it(18)+3*it(21)+2*s(8)+1*s(10)+1*s(11)+2
Such that:it(18) =< V-V1
it(16) =< V/3-V1/3
aux(38) =< V
aux(39) =< V+V1
aux(40) =< 2*V
aux(41) =< V/2
aux(42) =< V1
aux(43) =< 2*V1
s(11) =< aux(39)
it(16) =< aux(40)
it(16) =< aux(38)
it(17) =< aux(38)
it(18) =< aux(38)
it(21) =< aux(38)
s(8) =< aux(38)
it(18) =< aux(40)
it(21) =< aux(40)
it(16) =< aux(39)
it(18) =< aux(39)
it(21) =< aux(39)
it(17) =< aux(40)
it(16) =< aux(41)
it(18) =< aux(41)
aux(6) =< aux(38)*2
it(18) =< it(17)+aux(38)+aux(42)
s(10) =< it(17)*2+aux(6)+aux(43)
s(10) =< it(18)*aux(39)

with precondition: [V>=2,V1>=0,Out>=1,V>=Out]

* Chain [[16,17,18,21],19,23]: 3*it(16)+4*it(17)+3*it(18)+2*s(8)+1*s(10)+2*s(12)+3
Such that:it(18) =< V-V1
it(16) =< V/3-V1/3
aux(2) =< V1
aux(7) =< 2*V1
aux(44) =< V
aux(45) =< V+V1
aux(46) =< 2*V
aux(47) =< V/2
s(12) =< aux(45)
it(16) =< aux(46)
it(16) =< aux(44)
it(17) =< aux(44)
it(18) =< aux(44)
s(8) =< aux(44)
it(18) =< aux(46)
it(17) =< aux(46)
it(16) =< aux(45)
it(18) =< aux(45)
it(16) =< aux(47)
it(18) =< aux(47)
aux(6) =< aux(44)*2
it(18) =< it(17)+aux(44)+aux(2)
s(10) =< it(17)*2+aux(6)+aux(46)
s(10) =< it(17)*2+aux(6)+aux(7)
it(18) =< it(17)+aux(44)+aux(44)
s(10) =< it(18)*aux(45)

with precondition: [V>=2,V1>=0,Out>=3,2*V+2*V1>=Out+1]

* Chain [[16,17,18,21],19,22]: 3*it(16)+1*it(17)+3*it(18)+3*it(21)+2*s(8)+1*s(10)+2*s(12)+2
Such that:it(18) =< V-V1
aux(4) =< V-Out
aux(9) =< 2*V-2*Out
it(16) =< V/3-V1/3
aux(2) =< V1
aux(7) =< 2*V1
aux(49) =< V
aux(50) =< V+V1
aux(51) =< 2*V
aux(52) =< V/2
it(16) =< aux(51)
s(12) =< aux(50)
it(16) =< aux(49)
it(17) =< aux(49)
it(18) =< aux(49)
it(21) =< aux(49)
s(8) =< aux(49)
it(18) =< aux(51)
it(21) =< aux(51)
it(16) =< aux(50)
it(18) =< aux(50)
it(21) =< aux(50)
it(17) =< aux(51)
it(16) =< aux(52)
it(18) =< aux(52)
aux(6) =< aux(49)*2
it(18) =< it(17)+aux(49)+aux(2)
s(10) =< it(17)*2+aux(6)+aux(9)
s(10) =< it(17)*2+aux(6)+aux(7)
it(18) =< it(17)+aux(49)+aux(4)
s(10) =< it(18)*aux(50)

with precondition: [V>=2,V1>=0,Out>=1,V>=Out,V+V1>=Out+1]

* Chain [23]: 1
with precondition: [V=0,V1=Out,V1>=0]

* Chain [22]: 0
with precondition: [Out=0,V>=0,V1>=0]

* Chain [20,23]: 1*s(11)+3
Such that:s(11) =< V1

with precondition: [Out=1,V>=1,V1>=0]

* Chain [20,22]: 1*s(11)+2
Such that:s(11) =< V1

with precondition: [Out=1,V>=1,V1>=0]

* Chain [19,23]: 1*s(12)+1*s(13)+3
Such that:s(12) =< V1
s(13) =< Out/2

with precondition: [V>=1,Out>=3,2*V1+1>=Out]

* Chain [19,22]: 2*s(12)+2
Such that:aux(48) =< V1
s(12) =< aux(48)

with precondition: [Out=1,V>=1,V1>=1]


#### Cost of chains of start(V,V1):
* Chain [25]: 7*s(74)+13*s(76)+6*s(87)+12*s(88)+18*s(89)+6*s(91)+15*s(92)+9*s(93)+2*s(96)+4*s(97)+1*s(99)+3
Such that:s(99) =< V1+1/2
aux(63) =< V
aux(64) =< V-V1
aux(65) =< V+V1
aux(66) =< 2*V
aux(67) =< V/2
aux(68) =< V/3-V1/3
aux(69) =< V1
aux(70) =< 2*V1
s(76) =< aux(63)
s(87) =< aux(64)
s(88) =< aux(64)
s(89) =< aux(68)
s(74) =< aux(69)
s(91) =< aux(65)
s(89) =< aux(66)
s(89) =< aux(63)
s(92) =< aux(63)
s(87) =< aux(63)
s(87) =< aux(66)
s(92) =< aux(66)
s(89) =< aux(65)
s(87) =< aux(65)
s(89) =< aux(67)
s(87) =< aux(67)
s(95) =< aux(63)*2
s(87) =< s(92)+aux(63)+aux(69)
s(96) =< s(92)*2+s(95)+aux(66)
s(96) =< s(92)*2+s(95)+aux(70)
s(87) =< s(92)+aux(63)+aux(63)
s(96) =< s(87)*aux(65)
s(88) =< aux(63)
s(88) =< aux(66)
s(88) =< aux(65)
s(88) =< aux(67)
s(88) =< s(92)+aux(63)+aux(69)
s(97) =< s(92)*2+s(95)+aux(70)
s(97) =< s(88)*aux(65)
s(93) =< aux(63)
s(93) =< aux(66)
s(93) =< aux(65)

with precondition: [V>=0]

* Chain [24]: 1
with precondition: [V1=0,V>=0]


Closed-form bounds of start(V,V1):
-------------------------------------
* Chain [25] with precondition: [V>=0]
- Upper bound: 61*V+3+nat(V1)*7+4*V+nat(2*V1)*4+nat(V+V1)*6+nat(V1+1/2)+nat(V-V1)*18+nat(V/3-V1/3)*18
- Complexity: n
* Chain [24] with precondition: [V1=0,V>=0]
- Upper bound: 1
- Complexity: constant

### Maximum cost of start(V,V1): 61*V+2+nat(V1)*7+4*V+nat(2*V1)*4+nat(V+V1)*6+nat(V1+1/2)+nat(V-V1)*18+nat(V/3-V1/3)*18+1
Asymptotic class: n
* Total analysis performed in 676 ms.

(10) BOUNDS(1, n^1)